Innovative verification techniques used in the implementation of a third-generation 1.1GHz 64*b microprocessorMELAMED, Victor; STUIMER, Harry; WILKINS, David et al.Lecture notes in computer science. 2002, pp 360-363, issn 0302-9743, isbn 3-540-00141-7, 4 p.Conference Paper

Vers un système de modules à la Harper-Lillibridge-Leroy pour les spécifications formelles B = Towards a system of Harper Lillibridge Leroy type modules for B formal specificationsPETIT, Dorian; MARIANO, Georges; POIRRIEZ, Vincent et al.Journées francophones des langages applicatifs. 2002, pp 85-99, isbn 2-7261-1197-1, 15 p.Conference Paper

The key Establishment problemBLUNDO, Carlo; D'ARCO, Paolo.Foundations of security analysis and design II : FOSAD 2001/2002 tutorial lectures. Lecture notes in computer science. 2004, pp 44-90, issn 0302-9743, isbn 3-540-20955-7, 47 p.Book Chapter

Définition et réalisation d'un outil de vérification formelle de programmes LUSTRE: le système LESAR = Design and implementation of a formal verification tool for LUSTRE programs: the system LESARRatel, Christophe; Ouabdessalam, Farid.1992, 200 p.Thesis

Mechanized formal methods : Where next?RUSHBY, J.Lecture notes in computer science. 1999, pp 48-51, issn 0302-9743, isbn 3-540-66587-0, 2VolConference Paper

Robotic surgeryMURADORE, Riccardo; BRESOLIN, Davide; GERETTI, Luca et al.IEEE robotics & automation magazine. 2011, Vol 18, Num 3, pp 24-32, issn 1070-9932, 9 p.Article

Verification of event-based synchronization of SpecC description using difference decision diagramsSAKUNKONCHAK, Thanyapat; FUJITA, Masahiro.Lecture notes in computer science. 2002, issn 0302-9743, isbn 3-540-00141-7, p. 369Conference Paper

View from the fringe of the fringe (Extended Summary)JOHNSON, Steven D.Lecture notes in computer science. 2001, pp 1-12, issn 0302-9743, isbn 3-540-42541-1Conference Paper

Using simulated execution in verifying distributed algorithmsTOH NE WIN; ERNST, Michael D; GARLAND, Stephen J et al.Lecture notes in computer science. 2003, pp 283-297, issn 0302-9743, isbn 3-540-00348-7, 15 p.Conference Paper

Vacuity detection in temporal model checkingKUPFERMAN, Orna; VARDI, Moshe Y.International journal on software tools for technology transfer (Print). 2003, Vol 4, Num 2, pp 224-233, issn 1433-2779, 10 p.Conference Paper

Loop problems in sequential equivalence checkingRAHIM, Solaiman; RAMPON, Jerome; ROUZEYRE, Bruno et al.Sophia Antipolis forum on microelectronics. 2002, pp 52-57, 1Vol, 6 p.Conference Paper

An ontology for mobile agents in the context of formal verificationSALEM DA SILVA, Paulo; VIEIRA DE MELO, Ana Cristina.Lecture notes in computer science. 2005, pp 1500-1516, issn 0302-9743, isbn 3-540-29736-7, 2Vol, 17 p.Conference Paper

Lectures on formal methods and performance analysis (Berg en Dal, 3-7 July 2000, revised papers)Brinksma, Ed; Hermanns, Holger; Katoen, Joost-Pieter et al.Lecture notes in computer science. 2001, issn 0302-9743, isbn 3-540-42479-2, VI, 429 p, isbn 3-540-42479-2Conference Proceedings

Hiding more of hidden algebraGOGUEN, J; ROSU, G.Lecture notes in computer science. 1999, pp 1704-1719, issn 0302-9743, isbn 3-540-66587-0, 2VolConference Paper

Formal verification: Applications & case studiesROWE, M.Lecture notes in computer science. 1997, issn 0302-9743, isbn 3-540-63166-6, p. 11Conference Paper

Vérification formelle des circuits digitaux décrits en VHDL = Formal verification of digital circuits described in VHDLSalem, Ashraf; Borrione, Dominique.1992, 131 p.Thesis

Formal verification of module interfaces against real time specificationsCHAKRABARTI, Arindam; DASGUPTA, Pallab; CHAKRABARTI, P. P et al.Design automation conference. 2002, pp 141-145, isbn 1-58113-461-4, 5 p.Conference Paper

Handling special constructs in symbolic simulationKÖLBL, Alfred; KUKULA, James; ANTREICH, Kurt et al.Design automation conference. 2002, pp 105-110, isbn 1-58113-461-4, 6 p.Conference Paper

A translation of Statecharts to EsterelSEBIS, S. A; SHYAMASUNDAR, R. K; BHATTACHARJEE, A. K et al.Lecture notes in computer science. 1999, pp 983-1007, issn 0302-9743, isbn 3-540-66587-0, 2VolConference Paper

Proof confluent tableau calculiHÄHNLE, R; BECKERT, B.Lecture notes in computer science. 1999, pp 34-35, issn 0302-9743, isbn 3-540-66086-0Conference Paper

FATES 2003 : formal approaches to software testing (Montreal PQ, 6 October 2003, revised papers)Petrenko, Alexandre; Ulrich, Andreas.Lecture notes in computer science. 2004, issn 0302-9743, isbn 3-540-20894-1, VIII, 266 p, isbn 3-540-20894-1Conference Proceedings

A framework for superscalar microprocessor correctness statementsAAGAARD, Mark D; COOK, Byron; DAY, Nancy A et al.International journal on software tools for technology transfer (Print). 2003, Vol 4, Num 3, pp 298-312, issn 1433-2779, 15 p.Conference Paper

Epistemic logic in higher order logic : an experiment with COQLescanne, Pierre.2001, 9 p.Report

A formal framework for synthesis and verification of logic programsAVELLONE, Alessandro; FERRARI, Mauro; FIORENTINI, Camillo et al.Lecture notes in computer science. 2001, Vol 2042, pp 1-17, issn 0302-9743, isbn 3-540-42127-0Conference Paper

Formal methods and security evaluationBOLIGNANO, D.Lecture notes in computer science. 1999, issn 0302-9743, isbn 3-540-66463-7, p. 291Conference Paper